theory Design_Instantiation
imports "./Specification/Design_OpenSession"  
        "./Specification/Design_CloseSession"
        "./Specification/Design_InvokeCommand"
        "./Specification/Design_Memory"


begin

section" Instantiation and Its Proofs of Security Model"

definition system_initR :: "Sys_Config ⇒ StateR"
  where "system_initR sc ≡ let s0 = system_init sc in 
                              ⦇current = current s0,
                            TAs_state = TAs_state s0,
                            REE_state = REE_state s0,
                            TEE_state = TEE_state s0,
                            system_time = system_time s0,  
                            exec_prime = exec_prime s0,
                            IPC_driver = ⦇tamgr_fifo=(10::int),svchost_fifo=(11::int),
                                            tamgr_data=smc_ex_init,svchost_data=smc_ex_init⦈
                           ⦈"
(*we set the intital two fifo to value 10 and 11 randomly*)





consts s0r :: StateR

specification (s0r) 
  s0r_init: "s0r = system_initR sysconf"
  by simp


definition exec_eventR :: "EventR ⇒ (StateR × StateR) set" where
    "exec_eventR e ≡ {(s,s'). s'∈  (case e of 
           hyperc' (TEEC_INITIALIZECONTEXT tn tctext) ⇒{fst (TEEC_InitializeContextR sysconf s tn tctext)}|
           hyperc' (TEEC_FINALIZECONTEXT tctext) ⇒ {(TEEC_FinalizeContextR sysconf s tctext)}|
           hyperc' (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t) ⇒{fst(TEEC_OpenSession1R sysconf s tct tst uuid cm cd opt mem_t)}|
           hyperc' TEEC_OPENSESSION2 ⇒{fst (TEEC_OpenSession2R sysconf s)}|
           hyperc' (TEEC_OPENSESSION3 ses_id)⇒{fst (TEEC_OpenSession3R sysconf s ses_id)}|
           hyperc' (TEEC_OPENSESSION4)⇒{fst (TEEC_OpenSession4R sysconf s)}|
           hyperc' (TEE_OPENTASESSION1) ⇒{fst(TEE_OpenTASession1R sysconf s)}|
           hyperc' TEE_OPENTASESSION2 ⇒{fst (TEE_OpenTASession2R sysconf s)}|
           hyperc' (TEE_OPENTASESSION3 ses_id)⇒{fst (TEE_OpenTASession3R sysconf s ses_id)}|
           hyperc' (TEE_OPENTASESSION4)⇒{fst (TEE_OpenTASession4R sysconf s)}|
           hyperc' (TEEC_CLOSESESSION1 fd ses_id in_params out_params) ⇒{fst(TEEC_CloseSession1R sysconf s fd ses_id in_params out_params)}|
           hyperc' (TEEC_CLOSESESSION2) ⇒{fst(TEEC_CloseSession2R sysconf s)}|
           hyperc' (TEEC_CLOSESESSION3) ⇒{fst(TEEC_CloseSession3R sysconf s)}|
           hyperc' (TEEC_CLOSESESSION4) ⇒{fst(TEEC_CloseSession4R sysconf s)}|
           hyperc' (TEE_CLOSETASESSION1) ⇒{fst(TEE_CloseTASession1R sysconf s)}|
           hyperc' (TEE_CLOSETASESSION2) ⇒{fst(TEE_CloseTASession2R sysconf s)}|
           hyperc' (TEE_CLOSETASESSION3) ⇒{fst(TEE_CloseTASession3R sysconf s)}|
           hyperc' (TEE_CLOSETASESSION4) ⇒{fst(TEE_CloseTASession4R sysconf s)}|
           hyperc' (TEEC_INVOKECOMMAND1 ses_id time_out cmd_id in_params out_params memBlock_memRef) ⇒{fst(TEEC_InvokeCommand1R sysconf s ses_id time_out cmd_id in_params out_params memBlock_memRef)}|
           hyperc' (TEEC_INVOKECOMMAND2)⇒{fst(TEEC_InvokeCommand2R sysconf s)}|
           hyperc' (TEEC_INVOKECOMMAND3)⇒{fst(TEEC_InvokeCommand3R sysconf s)}|
           hyperc' (TEEC_INVOKECOMMAND4)⇒{fst(TEEC_InvokeCommand4R sysconf s)}|
           hyperc' (TEE_INVOKETACOMMAND1 memBlock_memRef) ⇒ {fst(TEE_InvokeTACommand1R sysconf s memBlock_memRef)}|
           hyperc' (TEE_INVOKETACOMMAND2) ⇒ {fst(TEE_InvokeTACommand2R sysconf s)}|
           hyperc' (TEE_INVOKETACOMMAND3) ⇒ {fst(TEE_InvokeTACommand3R sysconf s)}|
           hyperc' (TEE_INVOKETACOMMAND4) ⇒ {fst(TEE_InvokeTACommand4R sysconf s)}|
           hyperc' (TEE_CHECKMEMORYACCESSRIGHTS accessflags bid bsize) ⇒{s}|
           hyperc' (TEE_MALLOC bsize hi) ⇒{(TEE_MallocR sysconf s bsize hi)}|
           hyperc' (TEE_REALLOC bsize hi) ⇒{(TEE_ReallocR sysconf s bsize hi)}|
           hyperc' (TEE_FREE bid) ⇒{(TEE_FreeR sysconf s bid)}|
           hyperc' (TEEC_REGISTERSHAREDMEMORY tctext shared) ⇒{fst(TEEC_RegisterSharedMemoryR sysconf s tctext shared)}|
           hyperc' (TEEC_ALLOCATESHAREDMEMORY tctext shared) ⇒{fst(TEEC_AllocateSharedMemoryR sysconf s tctext shared)}|
           hyperc' (TEEC_RELEASESHAREDMEMORY shared) ⇒{(TEEC_ReleaseSharedMemoryR sysconf s shared)}|
           _ ⇒{s}
          
)}"



definition eR :: "EventR ⇒ Event" where
  "eR e ≡ 
      case e of hyperc' (TEEC_INITIALIZECONTEXT tn tctext) ⇒(hyperc (Hypercall.TEEC_INITIALIZECONTEXT tn tctext))|
           hyperc' (TEEC_FINALIZECONTEXT tctext) ⇒(hyperc (Hypercall.TEEC_FINALIZECONTEXT tctext))|
           hyperc' (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t) ⇒(hyperc (Hypercall.TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t))|
           hyperc' TEEC_OPENSESSION2 ⇒ (hyperc (Hypercall.TEEC_OPENSESSION2))|
           hyperc' (TEEC_OPENSESSION3 ses_id)⇒ (hyperc (Hypercall.TEEC_OPENSESSION3 ses_id))|
           hyperc' (TEEC_OPENSESSION4)⇒ (hyperc (Hypercall.TEEC_OPENSESSION4))|
           hyperc' TEE_OPENTASESSION1 ⇒ (hyperc (Hypercall.TEE_OPENTASESSION1))|
           hyperc' TEE_OPENTASESSION2⇒ (hyperc (Hypercall.TEE_OPENTASESSION2))|
           hyperc' (TEE_OPENTASESSION3 sid)⇒ (hyperc (Hypercall.TEE_OPENTASESSION3 sid))|
           hyperc' (TEE_OPENTASESSION4)⇒  (hyperc (Hypercall.TEE_OPENTASESSION4))|
           hyperc' (TEEC_CLOSESESSION1 fd ses_id in_params out_params) ⇒(hyperc (Hypercall.TEEC_CLOSESESSION1 fd ses_id in_params out_params))|
           hyperc' TEEC_CLOSESESSION2 ⇒  (hyperc (Hypercall.TEEC_CLOSESESSION2))|
           hyperc' TEEC_CLOSESESSION3 ⇒  (hyperc (Hypercall.TEEC_CLOSESESSION3))|
           hyperc' TEEC_CLOSESESSION4 ⇒  (hyperc (Hypercall.TEEC_CLOSESESSION4))|
           hyperc' TEE_CLOSETASESSION1⇒  (hyperc (Hypercall.TEE_CLOSETASESSION1))|
           hyperc' TEE_CLOSETASESSION2⇒  (hyperc (Hypercall.TEE_CLOSETASESSION2))|
           hyperc' TEE_CLOSETASESSION3⇒  (hyperc (Hypercall.TEE_CLOSETASESSION3))|
           hyperc' TEE_CLOSETASESSION4⇒  (hyperc (Hypercall.TEE_CLOSETASESSION4))|
           hyperc' (TEEC_INVOKECOMMAND1 ses_id timeout cmd pt1 pt2 mem_t) ⇒  (hyperc (Hypercall.TEEC_INVOKECOMMAND1 ses_id timeout cmd pt1 pt2 mem_t))|
           hyperc' TEEC_INVOKECOMMAND2⇒  (hyperc (Hypercall.TEEC_INVOKECOMMAND2))|
           hyperc' TEEC_INVOKECOMMAND3⇒  (hyperc (Hypercall.TEEC_INVOKECOMMAND3))|
           hyperc' TEEC_INVOKECOMMAND4⇒  (hyperc (Hypercall.TEEC_INVOKECOMMAND4))|
           hyperc' (TEE_INVOKETACOMMAND1 mem_t)⇒  (hyperc (Hypercall.TEE_INVOKETACOMMAND1 mem_t))|
           hyperc' TEE_INVOKETACOMMAND2⇒  (hyperc (Hypercall.TEE_INVOKETACOMMAND2))|
           hyperc' TEE_INVOKETACOMMAND3⇒  (hyperc (Hypercall.TEE_INVOKETACOMMAND3))|
           hyperc' TEE_INVOKETACOMMAND4⇒  (hyperc (Hypercall.TEE_INVOKETACOMMAND4))|
           hyperc' (TEE_CHECKMEMORYACCESSRIGHTS accessflags bid bsize) ⇒  (hyperc (Hypercall.TEE_CHECKMEMORYACCESSRIGHTS accessflags  bid bsize))|
           hyperc' (TEE_MALLOC bsize hi) ⇒  (hyperc (Hypercall.TEE_MALLOC bsize hi))|
           hyperc' (TEE_REALLOC mb bsize) ⇒  (hyperc (Hypercall.TEE_REALLOC mb bsize))|
           hyperc' (TEE_FREE bid) ⇒  (hyperc (Hypercall.TEE_FREE bid))|
           hyperc' (TEEC_REGISTERSHAREDMEMORY tctext shared) ⇒  (hyperc (Hypercall.TEEC_REGISTERSHAREDMEMORY tctext shared))|
           hyperc' (TEEC_ALLOCATESHAREDMEMORY tctext shared) ⇒  (hyperc (Hypercall.TEEC_ALLOCATESHAREDMEMORY tctext shared))|
           hyperc' (TEEC_RELEASESHAREDMEMORY shared) ⇒  (hyperc (Hypercall.TEEC_RELEASESHAREDMEMORY shared))|
           sys' Reserved ⇒ (sys (Syscall.Reserved))"

definition domain_of_eventR :: "StateR ⇒ EventR ⇒ DOMAIN_ID option" where 
    "domain_of_eventR s e ≡ Some (current s)"

(*used in property refinement definition*)
lemma domain_domainR : " domain_of_eventR s e = domain_of_event (⇑s) ( (eR e))"
  proof(induct e)
    case (hyperc' x) then show ?case 
      proof(induct x)
        qed(simp add:domain_of_eventR_def eR_def abstract_state_def)+ 
  next 
    case (sys' x) then show ?case 
      using abstract_state_def domain_of_eventR_def 
        by auto
  qed





(*observation function for new state variable, only TEE can see this*)
definition vpeq_ipc :: "StateR ⇒ DOMAIN_ID ⇒ StateR ⇒ bool" ("(_ ∼. _ .∼Δ _)")
  where "vpeq_ipc s d t ≡ if is_TEE sysconf d then 
                              (IPC_driver s =IPC_driver t)
                           else True"


lemma vpeq_ipc_transitive_lemma : 
  "∀ s t r d. (vpeq_ipc s d t) ∧ (vpeq_ipc t d r) ⟶ (vpeq_ipc s d r)"
  using vpeq_ipc_def by auto
  
lemma vpeq_ipc_symmetric_lemma : "∀ s t d. (vpeq_ipc s d t) ⟶ (vpeq_ipc t d s)"
  using vpeq_ipc_def by auto

lemma vpeq_ipc_reflexive_lemma : "∀ s d. (vpeq_ipc s d s)"
  using vpeq_ipc_def by auto

definition vpeqR :: "StateR ⇒ DOMAIN_ID ⇒ StateR ⇒ bool" ("(_ ∼. _ .∼ _)")
  where "vpeqR s d t ≡  ((⇑s) ∼d∼ (⇑t)) ∧ (s∼.d.∼Δt)"

declare vpeqR_def[cong] and vpeq_ipc_def[cong] and vpeq_ipc_transitive_lemma
              and vpeq_ipc_symmetric_lemma and vpeq_ipc_reflexive_lemma

lemma vpeqR_transitive_lemma : "∀ s t r d. (vpeqR s d t) ∧ (vpeqR t d r) ⟶ (vpeqR s d r)"
    apply(clarsimp cong del: vpeq1_def)
    using vpeq1_transitive vpeq_ipc_transitive_lemma by blast

lemma vpeqR_symmetric_lemma : "∀ s t d. (vpeqR s d t) ⟶ (vpeqR t d s)"
  apply(clarsimp cong del: vpeq1_def)
  using vpeq1_symmetric vpeq_ipc_symmetric_lemma by blast

lemma vpeqR_reflexive_lemma : "∀ s d. (vpeqR s d s)"  
  using vpeq1_reflexive vpeq_ipc_reflexive_lemma by auto

lemma vpeqR_vpeq1 : "vpeqR s d t ⟹ vpeq1 (⇑s) d (⇑t)"
  by fastforce


definition get_exec_primeR::"StateR⇒((EVENT_PARAM×EVENT_NAME) list ×TEE_TA_MANAGER × TAs_State)"where
          "get_exec_primeR s ≡ (exec_prime s,ta_mgr(TEE_state s),TAs_state s)"
          
definition get_elistR::"StateR⇒(EVENT_PARAM×EVENT_NAME) list"where
          "get_elistR s ≡ exec_prime s"

definition get_TA_domainR :: "StateR⇒TA_State_Type⇒DOMAIN_ID" where
        "get_TA_domainR s ta ≡ (SOME tid.  (the ((TAs_state s) tid)) = ta)"

definition TA_domainR :: "StateR⇒TA_State_Type⇒DOMAIN_ID" where
        "TA_domainR s ta ≡ get_TA_domainR s ta"


interpretation O_ISOLATION
        s0r exec_eventR domain_of_eventR get_exec_primeR vpeqR interference1 "TEE sysconf" "REE sysconf" TA_domainR
        using   vpeqR_transitive_lemma vpeqR_symmetric_lemma vpeqR_reflexive_lemma ins_tee_intf_all ins_no_intf_tee
             nintf_reflx  ins_reachable
             by (smt (verit, best) O_ISOLATION.intro) 



section "Event Specification"

declare abstract_state_def[cong] and abstract_state_rev_def[cong]
        TEEC_InitializeContextR_def[cong] TEEC_FinalizeContextR_def[cong]


section" Unwinding conditions on new state variables "

definition weak_confidentiality_new :: "bool" where
    "weak_confidentiality_new ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ (domain_of_eventR s a = domain_of_eventR t a)
                                ∧(get_exec_primeR s=get_exec_primeR t) ∧
                            ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
                            (∀ s' t'. (s,s') ∈ exec_eventR a ∧ (t,t') ∈ exec_eventR a ⟶ (s' ∼.d.∼Δ t'))"

  definition confidentiality_new :: "bool" where
    "confidentiality_new ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ (domain_of_eventR s a = domain_of_eventR t a)
                                ∧(get_exec_primeR s=get_exec_primeR t) ∧
                            ((the (domain_of_eventR s a)) ↝ d) ⟶ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
                            (∀ s' t'. (s,s') ∈ exec_eventR a ∧ (t,t') ∈ exec_eventR a ⟶ (s' ∼.d.∼Δ t'))"

  definition integrity_new :: "bool" where
    "integrity_new ≡ ∀ a d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s,s')∈exec_eventR a 
                                    ⟶ (s ∼. d .∼Δ s')"

  definition weak_confidentiality_new_e :: "EventR ⇒ bool" where
    "weak_confidentiality_new_e a ≡  ∀d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ (domain_of_eventR s a = domain_of_eventR t a)
                                ∧(get_exec_primeR s=get_exec_primeR t) ∧
                            ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
                            (∀ s' t'. (s,s') ∈ exec_eventR a ∧ (t,t') ∈ exec_eventR a ⟶ (s' ∼.d.∼Δ t'))"

  definition confidentiality_new_e :: "EventR ⇒ bool" where
    "confidentiality_new_e a ≡ ∀d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ (domain_of_eventR s a = domain_of_eventR t a)
                                ∧(get_exec_primeR s=get_exec_primeR t) ∧
                            ((the (domain_of_eventR s a)) ↝ d) ⟶ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
                            (∀ s' t'. (s,s') ∈ exec_eventR a ∧ (t,t') ∈ exec_eventR a ⟶ (s' ∼.d.∼Δ t'))"

  definition integrity_new_e :: "EventR ⇒ bool" where
    "integrity_new_e a ≡ ∀d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s,s')∈exec_eventR a 
                                    ⟶ (s ∼. d .∼Δ s')"

declare weak_confidentiality_new_def[cong del] and confidentiality_new_def[cong del] and integrity_new_def[cong del] and
        weak_confidentiality_new_e_def[cong del] and confidentiality_new_e_def[cong del] and integrity_new_e_def[cong del] 

declare weak_confidentiality_new_def[cong] and confidentiality_new_def[cong] and integrity_new_def[cong] and
        weak_confidentiality_new_e_def[cong] and confidentiality_new_e_def[cong] and integrity_new_e_def[cong] 

declare weak_confidentiality_new_def[cong del] and confidentiality_new_def[cong del] and integrity_new_def[cong del] and
        weak_confidentiality_new_e_def[cong del] and confidentiality_new_e_def[cong del] and integrity_new_e_def[cong del]

  lemma weak_confidentiality_new_all_evt : "weak_confidentiality_new = (∀a. weak_confidentiality_new_e a)"
    by (simp add:weak_confidentiality_new_def weak_confidentiality_new_e_def)

  lemma confidentiality_new_all_evt : "confidentiality_new = (∀a. confidentiality_new_e a)"
    by (simp add:confidentiality_new_def confidentiality_new_e_def)

  lemma integrity_new_all_evt : "integrity_new = (∀a. integrity_new_e a)"
    by (simp add:integrity_new_def integrity_new_e_def)

end